\section{Proof steps}
\label{sec:steps}


We now describe the possible steps that Zeno can apply to a goal.
 As we said earlier, each step reduces the current property into the conjunction of one or more simpler properties, or directly proves the property to be true.
 % A step is displayed with a three character identifier in Zeno's proof output.


\subsection{\li{[eql]} - Reflexivity of equality}

This step reduces the goal $\tau\ \lim{=}\ \tau\ \lim{:-}\ \equalities$ to \li{True}. That is,
 % to say
 if the two sides of the goal's consequent are syntactically equal, then the goal is trivially true. This step is trivially sound, because \textbf{HC} is a pure functional language, where syntactic equality implies  equality.\footnote{In an imperative language such a step would not be sound and  we would need to make its application  conditional on constancy annotations or framing.}
Examples of this step appear on lines 5 and 11 of the proof in \fig{proofaddzero}. % Line 5 expresses that we have reduced \li{0 = 0} to \li{True} using \li{[eql]}.

%\sidenote As this is a functional language identical function calls will always yield the same result, so this step will apply even when both sides of the consequent are a function call. This would not be the case in most imperative languages, where function calls may be affected by mutable external state.


\subsection{\li{[def]} - Applying function definitions}

This step applies function definitions, and thus reduces the goal to a simpler one.
%  through the usage of any applicable function definitions.
%If any terms within the goal can be evaluated to another term then they will
%be with this step.
This step is sound, because  function definitions can be seen as   background lemmas
for any proof and can be applied as such.

Examples of this step can be found on lines 4 and 9 of \fig{proofaddzero}. On line 9, for example, Zeno applied the definition of \li{(+)}, and reduced the term \li{S x' + 0} to the term \li{S (x' + 0)}.

\sidenote When trying to apply a function definition we can also use the antecedents of our goal to rewrite any case-analysed expressions. This is particularly useful after a \emph{case-split} step -- more later.


\subsection{\li{[ind x =>} $\tau$\li{]} - Proof by structural induction}

This step describes the inductive step where the variable \li{x}
% and that we are down the branch in which \li{x}
has the same value as term $\tau$. This line in the proof output will be followed by zero or more lines of the form ``\li{with} $\equality$'', one for each induction hypothesis $\equality$ added down this branch. Multiple nested \li{[ind]} steps represent the step by step construction of an induction scheme for a proof.

To apply structural induction on a variable \li{x} of a type \li{T}, Zeno constructs a separate proof branch for each constructor of \li{T}\footnote{Obviously, induction is not applicable for function types.}. For each such proof branch, and for each recursively typed argument of the branch's constructor,   Zeno adds an inductive hypothesis down that branch. The inductive hypotheses is identical to the original goal, except that the inductive variable \li{x} is replaced by each recursively typed argument variable in turn.

Lines 3 and 7 of our example proof in \fig{proofaddzero} represent the two branches needed for an inductive proof over \li{x}. As \li{x} is of type \li{Nat},  Zeno constructs one branch for each of the two constructors of \li{Nat}, i.e. one branch for when \li{x} is \li{0} and the other for  when \li{x} is \li{S x'} for some new \li{x'} of type \li{Nat}. Because \li{x'} has the same type as \li{x},  the inductive hypothesis down this branch is \li{x' + 0 = x'}, as shown by line 8.

One useful feature of inductive hypotheses is that every variable is universally quantified except for the inductive one, since every variable is implicitly universally quantified in the goal from which it was generated. Take for example the property \li{x + y = y + x}, which is really $\forall \lim{x} . \forall \lim{y} . \lim{x + y = y + x}$. If Zeno were to perform induction on \li{x} then down the \li{S x'} branch it would get the hypothesis $\forall \lim{y} . \lim{x' + y = y + x'}$. It can then match any variable to the \li{y} when using this hypothesis, rather than just the original \li{y} from the goal. 

In order that this preserve a well-founded ordering for our induction scheme when a variable is inducted upon, if it exists $\forall$-quantified in an existing induction hypothesis this quantifier is removed and the variable replaced with its new value down this branch. For example if we had the induction hypothesis $\forall \lim{y} . \lim{x' + y = y + x'}$ and we perform an induction step on \li{y}, down the branch \li{[ind y => 0]} this hypothesis would become \li{x' + 0 = 0 + x'}.


\subsection{\li{[hyp} $\equality$\li{]} - Application of an inductive hypothesis}

This step  reduces the goal by applying the induction hypothesis $\equality$ as a rewrite rule to the goal. On line 9 of \fig{proofaddzero} Zeno  reduced the goal \li{S (x' + 0)} to \li{S x'} by using the hypothesis \li{x' + 0 = x'}.

\sidenote When  performing induction on a goal with antecedents, Zeno creates a hypothesis which also has antecedents. This means we can only apply the hypothesis if the antecedents have been satisfied by the antecedents of the current goal. An example of this could be seen in Zeno's proof of that \li{(<=)} is a total ordering, i.e. \li{x <= y = True :- y <= x = False}\footnote{This is not detailed here but can be seen by proving \li{prop_nat_leq_total} on TryZeno \url{http://www.doc.ic.ac.uk/~ws506/tryzeno}}.


\begin{figure}[h]
\begin{lstlisting}[basicstyle=\ttfamily\footnotesize]
rev (rev xs) = xs
 ...
 > [hyp ...] rev (rev xs' ++ (x : [])) = x : rev (rev xs')
 > [gen rev xs' => ys] rev (ys ++ (x : [])) = x : rev ys
 ...
Proven: rev (ys ++ (x : [])) = x : rev ys
        rev (rev xs) = xs
\end{lstlisting}
\caption{Generalization discovers auxiliary lemmas - highlighted example}
\label{fig:revrevgenex}
\end{figure}


\subsection{\li{[gen} $\tau$ \li{ => x]} - Generalising term $\tau$ to variable \li{x}}
\label{sec:steps:generalisation}
 
This step reduces a goal to a more general one by replacing all instances of a sub-term $\tau$ in the goal with a new variable \li{x}. For example, the application of \li{[gen x + y => z]} on \li{(x + y)} \li{+ 0 = x + y} gives us \li{z + 0 = z}.

Generalisation is a well established technique in inductive theorem proving\cite{productivefailure} and is often how we discover important auxiliary lemmas within our proofs. For example, the proof that the application of list reversal twice returns the original list, as seen in our shortened proof in \fig{revrevgenex}, depends on the auxiliary lemma \li{rev (ys ++ (x : []))} \li{= x : rev ys}, which is ``discovered''  by our generalisation step and subsequently proven.


\subsection{\li{[fac]} - Goal factoring}

Goal factoring is applicable on goals where the same function appears outermost on both sides of the equation of the consequent. For example, \li{(x + 0)} \li{+ y = x + y},   can be factored to  \li{x + 0 = x} and \li{y = y}.

The formal presentation of this step demonstrates its soundness:

$ ~ $ \hspace{1in}
$\bigwedge_i (\clause{\tau_i = \tau_i'}{\equalities}) \quad \Rightarrow \quad (\clause{f\ \vect{\tau} = f\ \vect{\tau'}}{\equalities}) $



% SD Chopped: goes without saying
% If we are unable to complete the factored proofs then we can simply continue on with the original proof. We believe this step to be sound from the intuitive soundness of its formalisation above.

\begin{figure}[h]
\begin{lstlisting}[numbers=left, basicstyle=\ttfamily\footnotesize]
[goal] max x 0 = x

 > [cse x <= 0 => False] max x 0 = x :- x <= 0 = False
 > [def] x = x :- x <= 0 = False
 > [eql] True

 > [cse x <= 0 => True] max x 0 = x :- x <= 0 = True
 > [def] 0 = x :- x <= 0 = True

  >> [ind x => 0] 0 = 0 :- 0 <= 0 = True
  >> [def] 0 = 0 :- True = True
  >> [eql] True

  >> [ind x => S x'] 0 = S x' :- S x' <= 0 = True
      + 0 = x' :- x' <= 0 = True
  >> [def] 0 = S x' :- False = True
  >> [con] True

Proven: 0 = x :- x <= 0 = True
        max x 0 = x
\end{lstlisting}
\caption{Proof that \li{0} is a right-identity for \li{max}}
\label{fig:proofmaxzero}
\end{figure}


\subsection{\li{[cse} $\tau$ \li{=>} $\tau'$\li{]} - Case-split on $\tau$}

This step corresponds  to case-splitting on a term $\tau$, and in particular to the branch where   $\tau$ is taken to have the form $\tau'$.
In case-splitting, as with induction, Zeno creates one branch for each different constructor of the type of $\tau$.
   Zeno then adds the equality $\tau = \tau'$ to the antecedents of the goal.
   
Case-splitting is sound, because the branches created cover all the possible values for the evaluation of $\tau$, and thus corresponds to  $\vee$-elimination from classical logic.

% This step is similar to generalisation (\S \ref{sec:steps:generalisation}) in that we prove a property to be true regardless of the value of a term, though we now consider each different value in a separate branch. With this in mind we believe our case-split step to be sound for the same reason as with generalisation, in that if we have proven a property regardless of the value of a term then we have proven it in general.

Lines 3 and 7 of the   proof in \fig{proofmaxzero} represent the two branches of a case-split on the term \li{x <= 0}. Line 3 introduces the branch in which \li{x <= 0} is \li{False}, and line 7 introduces the branch in which it is \li{True}. On line 4 Zeno then uses the new antecedent to apply the definition of \li{max} to the term \li{max x 0}, reducing it to \li{x}.


\subsection{\li{[con]} - Contradiction}
\label{sec:steps:con}

This step reduces a goal to \li{True} by finding a contradiction in its antecedents, and is  sound because $\bot \Rightarrow \equality$ is true for any $\equality$, even a false $\equality$.

A contradiction is found when we have an equality between two different constructor terms in one of our antecedents.
% , e.g. $\lim{0} \neq \lim{S x}$ regardless of the value of \li{x}. 
In the last line of \fig{proofmaxzero} we have proven our goal to be true since \li{False = True} is in the antecedents. 


\subsection{\li{[hcn} $\equality$\li{]} - Adding an inductive hypothesis to the goal conditions}

This step moves an inductive hypothesis from the background into the explicit list of goal conditions. This is necessary for proofs such as the verification of insertion sort i.e., \li{sorted (isort xs)} \li{= True} in \fig{verifyisort} where, combined with generalisation, it gives us the more easily proven sub-goal \li{sorted (insert y zs)} \li{= True :- sorted ys = True}.

\begin{figure}[h]
\begin{lstlisting}[basicstyle=\ttfamily\footnotesize]
[goal] sorted (isort xs) = True

 > [ind xs => y : ys] sorted (isort (y : ys)) = True
     with sorted (isort ys) = True
 > [def] sorted (insert y (isort ys)) = True
 > [hcn sorted (isort ys) = True] 
     sorted (insert y (isort ys)) = True 
       :- sorted (isort ys) = True
 > [gen isort ys => zs] 
     sorted (insert y zs) = True :- sorted zs = True
 ...
 
Proven: sorted (insert y zs) = True :- sorted zs = True
        sorted (isort xs) = True
\end{lstlisting}
\caption{Highlighted proof that insertion sort (\li{isort}) produces a \li{sorted} list}
\label{fig:verifyisort}
\end{figure}


\subsection{\li{[icn} $\equality$\li{]} - Inferring a new goal condition}

This step adds a new goal condition $\equality$ by inferring it from the existing conditions. This step is used instead of a case-split when one case is a theorem of the goal conditions. Whenever Zeno is going to use a case-split on a term $\tau$ it will first check whether it can be proven that $\tau\ \lim{=}\ \tau'$ for any $\tau'$ that is a constructor term of the type of $\tau$. 

As an example in \fig{icnex} we have a proof of \li{max x y = y :- y <= x = False}, as in \fig{proofmaxzero} the first step would be a case-split on \li{x <= y}. Zeno however can prove \li{x <= y = True :- y <= x = False}, meaning that the \li{x <= y = True} branch is a theorem of the conditions of the goal so we can discount the other branches. This step will always have two branches, the first one showing the inference proof and the second continuing the original proof with this new condition. 

\begin{figure}[h]
\begin{lstlisting}[basicstyle=\ttfamily\footnotesize]
[goal] max x y = y :- y <= x = False

  [icn] x <= y = True :- y <= x = False
  ...
  
  [icn x <= y = True] 
    max x y = y :- y <= x = False, x <= y = True
  [def] y = y :- y <= x = False, x <= y = True
  [eql] True
  
Proven: x <= y = True :- y <= x = False
        max x y = y :- y <= x = False
\end{lstlisting}
\caption{Inferring a new goal condition - highlighted example}
\label{fig:icnex}
\end{figure}

